|
System L is a natural deductive logic developed by E.J. Lemmon.〔See for an introductory presentation of Lemmon's natural deduction system.〕 Derived from Suppes' method,〔See , for an introductory presentation of Suppes' natural deduction system.〕 it represents natural deduction proofs as sequences of justified steps. Both methods are derived from Gentzen's 1934/1935 natural deduction system,〔, .〕 in which proofs were presented in tree-diagram form rather than in the tabular form of Suppes and Lemmon. Although the tree-diagram layout has advantages for philosophical and educational purposes, the tabular layout is much more convenient for practical applications. A similar tabular layout is presented by Kleene.〔.〕 The main difference is that Kleene does not abbreviate the left hand sides of assertions to line numbers, preferring instead to either give full lists of precedent propositions or alternatively indicate the left hand sides by bars running down the left of the table to indicate dependencies. However, Kleene's version has the advantage that it is presented, although only very sketchily, within a rigorous framework of metamathematical theory, whereas the books by Suppes〔 and Lemmon〔 are applications of the tabular layout for teaching introductory logic. == Description of the deductive system == The syntax of proof is governed by nine primitive rules: # The Rule of Assumption (A) # Modus Ponendo Ponens (MPP) # The Rule of Double Negation (DN) # The Rule of Conditional Proof (CP) # The Rule of ∧-introduction (∧I) # The Rule of ∧-elimination (∧E) # The Rule of ∨-introduction (∨I) # The Rule of ∨-elimination (∨E) # Reductio Ad Absurdum (RAA) In system L, a proof has a definition with the following conditions: # has a finite sequence of well-formed formulas (or ''wffs'') # each line of it is justified by a rule of the system L # the last line of the proof is what is intended, and this last line of the proof uses only the premises which were given, if any. If no premise is given, the sequent is called theorem. Therefore, the definition of a theorem in system L is: *a theorem is a sequent that can be proved in system L, using an empty set of assumptions. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「System L」の詳細全文を読む スポンサード リンク
|